S. Valentini; 1983; "The Modal Logic of Provability: Cut-Elimination"
メモ
証明可能性論理GLのシークエント計算体系
のカット除去定理について.
G. Gentzen; "Untersuchungen über das logische Schließen"
では
カット式
のdegree
と
証明図の高さ
による2重の帰納法なのに対し
こちらは更に
カット式のwidth
を足した3重の帰納法になっている.
いくつかスケッチレベルの証明があるらしいので,詳しくは後の時代の
R. Goré, R. Ramanayake; 2008; "Valentini's Cut-Elimination for Provability Logic Resolved"
を読んだほうが良いかも知らない.